#pragma once

#include <cstdint>
#include <exception>
#include <iostream>
#include <unordered_map>
#include <vector>

#include <mockturtle/mockturtle.hpp>

template<class TT>
bool maj_top_decomposition( const TT& tt, uint32_t var_index, TT* func_co0 = nullptr, TT* func_co1 = nullptr )
{
  /*try top maj decomposition*/
  static_assert( kitty::is_complete_truth_table<TT>::value, "Can only be applied on complete truth tables." );
  const auto co0 = cofactor0( tt, var_index );
  const auto co1 = cofactor1( tt, var_index );
  std::vector<uint8_t> support_co0;
  std::vector<uint8_t> support_co1;
  for ( auto s_sd = 0u; s_sd < co0.num_vars(); ++s_sd )
  {
    if ( kitty::has_var( co0, s_sd ) )
    {
      support_co0.push_back( s_sd );
    }
  }
  for ( auto s_sd = 0u; s_sd < co1.num_vars(); ++s_sd )
  {
    if ( kitty::has_var( co1, s_sd ) )
    {
      support_co1.push_back( s_sd );
    }
  }

  for ( auto i = 0u; i < support_co0.size(); ++i )
  {
    for ( auto j = 0u; j < support_co0.size(); ++j )
    {
      if ( support_co0[i] == support_co1[j] )
      {
        return false;
      }
    }
  }

  if ( is_const0( binary_and( co0, ~co1 ) ) )
  {
    if ( func_co0 )
    {
      *func_co0 = co0;
    }
    if ( func_co1 )
    {
      *func_co1 = co1;
    }
    return true;
  }
  return false;
}

template<class TT>
int maj_bottom_decomposition( const TT& tt, uint32_t var_index1, uint32_t var_index2, uint32_t var_index3, TT* func = nullptr )
{
  /*try botom maj decomposition*/
  static_assert( kitty::is_complete_truth_table<TT>::value, "Can only be applied on complete truth tables." );

  const auto co0_var1 = cofactor0( tt, var_index1 );
  const auto co1_var1 = cofactor1( tt, var_index1 );
  const auto dif_var1 = kitty::binary_xor( co0_var1, co1_var1 );

  const auto co0_var2 = cofactor0( tt, var_index2 );
  const auto co1_var2 = cofactor1( tt, var_index2 );
  const auto dif_var2 = kitty::binary_xor( co0_var2, co1_var2 );

  const auto co0_var3 = cofactor0( tt, var_index3 );
  const auto co1_var3 = cofactor1( tt, var_index3 );
  const auto dif_var3 = kitty::binary_xor( co0_var3, co1_var3 );

  const auto dif1_co0 = cofactor0( cofactor0( dif_var1, var_index2 ), var_index3 );
  const auto dif2_co0 = cofactor0( cofactor0( dif_var2, var_index1 ), var_index3 );
  const auto dif3_co0 = cofactor0( cofactor0( dif_var3, var_index1 ), var_index2 );

  const auto isconst01 = is_const0( dif1_co0 );
  const auto isconst02 = is_const0( dif2_co0 );
  const auto isconst03 = is_const0( dif3_co0 );

  // const auto num_pairs =
  //     static_cast<uint32_t>( isconst01 ) +
  //     static_cast<uint32_t>( isconst02 ) +
  //     static_cast<uint32_t>( isconst03 );

  const auto eq12 = equal( dif1_co0, dif2_co0 );
  const auto eq13 = equal( dif1_co0, dif3_co0 );
  const auto eq23 = equal( dif2_co0, dif3_co0 );

  const auto co0_var2_dif1 = cofactor0( dif_var1, var_index2 );
  const auto co1_var2_dif1 = cofactor1( dif_var1, var_index2 );
  const auto dif_var1_var2 = kitty::binary_xor( co0_var2_dif1, co1_var2_dif1 );

  const auto co0_var3_dif1 = cofactor0( dif_var1, var_index3 );
  const auto co1_var3_dif1 = cofactor1( dif_var1, var_index3 );
  const auto dif_var1_var3 = kitty::binary_xor( co0_var3_dif1, co1_var3_dif1 );

  const auto co0_var3_dif2 = cofactor0( dif_var2, var_index3 );
  const auto co1_var3_dif2 = cofactor1( dif_var2, var_index3 );
  const auto dif_var2_var3 = kitty::binary_xor( co0_var3_dif2, co1_var3_dif2 );

  if ( equal( dif_var1_var2, dif_var1_var3 ) && equal( dif_var1_var2, dif_var2_var3 ) && ( is_const0( ~dif_var1_var2 ) ) )
  {
    if ( is_const0( dif1_co0 ) && is_const0( dif2_co0 ) && is_const0( dif3_co0 ) )
    {
      auto co0_var1_co0_var2 = cofactor0( cofactor0( tt, var_index1 ), var_index2 );
      auto co0_var2_co1_var3_dif1 = cofactor1( cofactor0( dif_var1, var_index2 ), var_index3 );
      kitty::dynamic_truth_table tt_1( co0_var2_co1_var3_dif1.num_vars() );
      if ( func )
      {
        *func = kitty::binary_xor( mux_var( var_index1, co0_var2_co1_var3_dif1, tt_1 ), co0_var1_co0_var2 );
      }
      return 0;
    }
    if ( eq23 && isconst01 && ( is_const0( ~dif2_co0 ) ) )
    {
      auto co0_var1_co0_var2 = cofactor0( cofactor0( tt, var_index2 ), var_index3 );
      auto co0_var2_co1_var3_dif1 = cofactor0( cofactor1( dif_var1, var_index3 ), var_index2 );
      kitty::dynamic_truth_table tt_1( co0_var2_co1_var3_dif1.num_vars() );
      if ( func )
      {
        *func = kitty::binary_xor( mux_var( var_index1, co0_var2_co1_var3_dif1, tt_1 ), co0_var1_co0_var2 );
      }
      return 1;
    }
    if ( eq13 && isconst02 && ( is_const0( ~dif1_co0 ) ) )
    {
      auto co0_var1_co0_var2 = cofactor0( cofactor0( tt, var_index1 ), var_index3 );
      auto co0_var2_co1_var3_dif1 = cofactor0( cofactor1( dif_var2, var_index1 ), var_index3 );
      kitty::dynamic_truth_table tt_1( co0_var2_co1_var3_dif1.num_vars() );
      if ( func )
      {
        *func = kitty::binary_xor( mux_var( var_index1, co0_var2_co1_var3_dif1, tt_1 ), co0_var1_co0_var2 );
      }
      return 2;
    }
    if ( eq12 && isconst03 && ( is_const0( ~dif1_co0 ) ) )
    {
      auto co0_var1_co0_var2 = cofactor0( cofactor0( tt, var_index1 ), var_index2 );
      auto co0_var2_co1_var3_dif1 = cofactor0( cofactor1( dif_var3, var_index1 ), var_index2 );
      kitty::dynamic_truth_table tt_1( co0_var2_co1_var3_dif1.num_vars() );
      if ( func )
      {
        *func = kitty::binary_xor( mux_var( var_index1, co0_var2_co1_var3_dif1, tt_1 ), co0_var1_co0_var2 );
      }
      return 3;
    }
  }
  return -1;
}

